P, Q:. (P  Q)  ((P)  (Q)) 

latex

Up	core 2, core 2
Definitions	t  T, P  Q, P & Q, A, P  Q, P  Q, , x:A. B(x)
Lemmas	iff wf, false wf